Model checkers are tools that permit automatic model checking. Model checking typically verifies formal systems algorithmically. Formally specified models are fed into the model checkers, and the model checkers generate the state space that the model will traverse in its original run. Verifying any property of that model reduces to finding a path to reach a bad state from the initial state. A common problem faced by explicit state model checkers is a combinatorial blow up of the state space, commonly known as state space explosion.
The Spin model checker provides a specification language Promela. The Spin model checker is an efficient verification system for models of distributed software systems. It has been used to detect design errors in applications ranging from high-level descriptions of distributed algorithms to detailed code for controlling telephone exchanges.
Promela is a verification modeling language. It provides a way for making abstractions of distributed systems. The Spin model checker is frequently used to fractionally verify process behaviors that are considered suspect. A complete verification is, therefore, typically performed in a series of steps, with the construction of increasingly detailed Promela models. Each model can be verified with the Spin model checker under different types of assumptions about the environment. Once the correctness of a model has been established with the Spin model checker, that fact can be used in the construction and verification of all subsequent models.
Promela programs typically consist of processes, message channels, and variables. Processes are global objects that represent the concurrent entities of the distributed system. Message channels and variables can be declared either globally or locally within a process. The Promela syntax has a special data type, called “chan,” that may be used to model communication channels.
This “chan” data type allows the specification of two different types of communications, asynchronous (point to point) and synchronous (handshake). Point to point communications involve communications between two specific points or nodes. A handshake communication typically occurs at the beginning of a session between communicating entities. The handshake ensures that the two entities agree on how the transmission will proceed between them. Accordingly, in a handshake (or synchronous) communication between a single transmitter and a single receiver, the transmitter must wait for the receiver to receive the message from the channel before the transmitter can continue operation.
However, this “chan” data type has not been used to model either broadcast or multicast communications. Broadcast communications involve the transmission of a signal to the entire set of recipients in the system or service area. Multicast communications involve the transmission of a signal to a selected sub-set of recipients who belong to the appropriate multicast group.
In the literature, there have been references to the modeling of broadcast or multicast communications using a shared variable, but there have been no references to the modeling of all four types of communications, i.e., point to point communications, broadcast communications, multicast communications, and handshake communications, using the same channel. However, as a practical matter, all four type of communications do take place over the same channel.
More specifically, R. de Renesse and A. H. Aghvami, in “Formal Verification of Ad-Hoc Routing Protocols Using Spin Model Checker,” IEEE Melecon, 2004, modeled broadcast communications using as many channels as the number of processes. Thus, the common bus was replaced by several “point to point” channels, and a broadcast packet was transmitted synchronously through all channels. This modeling technique significantly increased the state space.
Henrik Ejersbo Jensen, Kim G. Larsen and Arne Skou, in “Modeling and Analysis of a Collision Avoidance Protocol using SPIN and UPPAAL,” SPIN 1996, considered a similar model with a separate process for the bus. That process ensures different types of communications using different flags. In effect, the bus is replaced by several “point to point” channels. Therefore, a common shared bus is not modeled in its true sense.
Michiel van Osch and Scott A. Smolka, in “Finite-State Analysis of the CAN Bus Protocol,” Proceedings of Sixth IEEE International Symposium on High Assurance Systems Engineering, HASE 2001, modeled the broadcast communication using a shared variable for the bus. This modeling technique does not blow up the state space, but it does not use the channels. Therefore, this modeling technique cannot be used to model handshake communications.
A model is disclosed herein that permits point to point communications, broadcast communications, multicast communications, and/or handshake communications using the same channel.